@misc{berdine05symbolic,
  author = "J. Berdine and C. Calcagno and P. O'Hearn",
  title = "Symbolic execution with separation logic",
  text = "Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. Symbolic execution
    with separation logic. In K. Yi, editor, APLAS 2005.",
  year = "2005",
  url = "citeseer.ist.psu.edu/berdine05symbolic.html" }

@InProceedings{BerdineCO05,
	Author		= {Josh Berdine and Cristiano Calcagno and Peter W. O'Hearn},
	Title		= {Smallfoot: Modular Automatic Assertion Checking with Separation Logic.},
	BookTitle	= {FMCO},
	EE		= {\url{http://dx.doi.org/10.1007/11804192_6}},
	Pages		= {115-137},
	Year		= 2005
}


@misc{ reynolds02separation,
  author = "J. Reynolds",
  title = "Separation logic: a logic for shared mutable data structures",
  text = "J. C. Reynolds. Separation logic: a logic for shared mutable data structures.
    Invited Paper, LICS'02, 2002. 29",
  year = "2002",
  url = "citeseer.ist.psu.edu/reynolds02separation.html" }

@book{GoMe93,
  key         ={GoMe93},
  author      ={M.J.C. Gordon and T.F. Melham},
  title       ={Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic},
  publisher   ={Cambridge University},
  year        =1993
}